Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	app(app(map,f),nil)	→ nil
2:	app(app(map,f),app(app(cons,x),xs))	→ app(app(cons,app(f,x)),app(app(map,f),xs))

There are 4 dependency pairs:


3:	APP(app(map,f),app(app(cons,x),xs))	→ APP(app(cons,app(f,x)),app(app(map,f),xs))
4:	APP(app(map,f),app(app(cons,x),xs))	→ APP(cons,app(f,x))
5:	APP(app(map,f),app(app(cons,x),xs))	→ APP(f,x)
6:	APP(app(map,f),app(app(cons,x),xs))	→ APP(app(map,f),xs)

The approximated dependency graph contains one SCC: {3,5,6}.

Tyrolean Termination Tool (0.06 seconds) --- May 4, 2006